(set-logic QF_LRA)
(set-info :source | TTA Startup. Bruno Dutertre (bruno@csl.sri.com) |)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun x_0 () Real)
(declare-fun x_1 () Real)
(declare-fun x_2 () Real)
(declare-fun x_3 () Real)
(declare-fun x_4 () Real)
(declare-fun x_5 () Real)
(declare-fun x_6 () Real)
(declare-fun x_7 () Real)
(declare-fun x_8 () Real)
(declare-fun x_9 () Bool)
(declare-fun x_10 () Bool)
(declare-fun x_11 () Bool)
(declare-fun x_12 () Bool)
(declare-fun x_13 () Real)
(declare-fun x_14 () Bool)
(declare-fun x_15 () Bool)
(declare-fun x_16 () Bool)
(declare-fun x_17 () Real)
(declare-fun x_18 () Real)
(declare-fun x_19 () Real)
(declare-fun x_20 () Real)
(declare-fun x_21 () Real)
(declare-fun x_22 () Real)
(declare-fun x_23 () Real)
(declare-fun x_24 () Real)
(declare-fun x_25 () Real)
(declare-fun x_26 () Real)
(declare-fun x_27 () Real)
(declare-fun x_28 () Real)
(declare-fun x_29 () Real)
(declare-fun x_30 () Real)
(declare-fun x_31 () Real)
(declare-fun x_32 () Real)
(declare-fun x_33 () Real)
(declare-fun x_34 () Real)
(declare-fun x_35 () Real)
(declare-fun x_36 () Real)
(declare-fun x_37 () Real)
(declare-fun x_38 () Real)
(declare-fun x_39 () Real)
(declare-fun x_40 () Real)
(declare-fun x_41 () Real)
(declare-fun x_42 () Real)
(declare-fun x_43 () Real)
(declare-fun x_44 () Real)
(declare-fun x_45 () Bool)
(declare-fun x_46 () Real)
(declare-fun x_47 () Bool)
(declare-fun x_48 () Bool)
(declare-fun x_49 () Bool)
(declare-fun x_50 () Real)
(declare-fun x_51 () Real)
(declare-fun x_52 () Real)
(declare-fun x_53 () Real)
(declare-fun x_54 () Real)
(declare-fun x_55 () Real)
(declare-fun x_56 () Real)
(declare-fun x_57 () Real)
(declare-fun x_58 () Real)
(declare-fun x_59 () Real)
(declare-fun x_60 () Real)
(assert (let ((?v_76 (= x_0 0)) (?v_91 (= x_0 1)) (?v_96 (= x_0 2)) (?v_122 (= x_1 0)) (?v_129 (= x_1 1)) (?v_133 (= x_1 2)) (?v_145 (= x_2 0)) (?v_152 (= x_2 1)) (?v_155 (= x_2 2)) (?v_165 (= x_3 0)) (?v_172 (= x_3 1)) (?v_175 (= x_3 2)) (?v_164 (= x_2 3)) (?v_184 (= x_3 3)) (?v_95 (= x_8 0)) (?v_112 (= x_0 3)) (?v_144 (= x_1 3)) (?v_1 (= x_13 4)) (?v_2 (= x_13 3)) (?v_3 (= x_13 2)) (?v_61 (not x_9)) (?v_62 (not x_10)) (?v_63 (not x_11)) (?v_64 (not x_12)) (?v_225 (not (< x_29 (+ x_30 24)))) (?v_227 (not (< x_31 (+ x_30 27)))) (?v_229 (not (< x_32 (+ x_30 30)))) (?v_231 (not (< x_33 (+ x_30 33)))) (?v_77 (= x_34 1)) (?v_89 (= x_34 2)) (?v_123 (= x_35 1)) (?v_126 (= x_35 2)) (?v_146 (= x_36 1)) (?v_149 (= x_36 2)) (?v_166 (= x_37 1)) (?v_169 (= x_37 2))) (let ((?v_196 (not ?v_77)) (?v_192 (not ?v_89)) (?v_197 (not ?v_123)) (?v_193 (not ?v_126)) (?v_198 (not ?v_146)) (?v_194 (not ?v_149)) (?v_199 (not ?v_166)) (?v_195 (not ?v_169)) (?v_18 (= x_36 3))) (let ((?v_26 (not ?v_18)) (?v_28 (not (= x_28 x_32))) (?v_19 (= x_37 3))) (let ((?v_29 (not ?v_19)) (?v_31 (not (= x_28 x_33))) (?v_211 (not (<= (- x_31 x_29) x_17))) (?v_212 (not (<= (- x_32 x_29) x_17))) (?v_213 (not (<= (- x_33 x_29) x_17))) (?v_214 (not (<= (- x_32 x_31) x_17))) (?v_215 (not (<= (- x_33 x_31) x_17))) (?v_216 (not (<= (- x_33 x_32) x_17))) (?v_220 (not (< (- x_29 x_30) 12))) (?v_207 (<= (- x_29 x_28) 12)) (?v_221 (not (< (- x_31 x_30) 15))) (?v_208 (<= (- x_31 x_28) 15)) (?v_222 (not (< (- x_32 x_30) 18))) (?v_209 (<= (- x_32 x_28) 18)) (?v_223 (not (< (- x_33 x_30) 21))) (?v_210 (<= (- x_33 x_28) 21)) (?v_24 (= x_39 x_40)) (?v_27 (= x_39 x_41)) (?v_30 (= x_39 x_42)) (?v_33 (= x_40 x_39)) (?v_37 (= x_40 x_41)) (?v_40 (= x_40 x_42)) (?v_42 (= x_41 x_39)) (?v_43 (= x_41 x_40)) (?v_44 (= x_41 x_42)) (?v_45 (= x_42 x_39)) (?v_46 (= x_42 x_40)) (?v_47 (= x_42 x_41)) (?v_22 (not (< x_28 x_29))) (?v_239 (= x_39 x_44)) (?v_32 (not (< x_28 x_31))) (?v_241 (= x_40 x_44)) (?v_36 (not (< x_28 x_32))) (?v_243 (= x_41 x_44)) (?v_39 (not (< x_28 x_33))) (?v_245 (= x_42 x_44)) (?v_15 (= x_34 3))) (let ((?v_20 (not ?v_15)) (?v_23 (not (= x_28 x_29))) (?v_16 (= x_35 3))) (let ((?v_21 (not ?v_16)) (?v_25 (not (= x_28 x_31))) (?v_224 (and x_45 (< x_46 x_29))) (?v_226 (and x_47 (< x_46 x_31))) (?v_228 (and x_48 (< x_46 x_32))) (?v_230 (and x_49 (< x_46 x_33))) (?v_8 (= x_44 4)) (?v_9 (= x_44 3)) (?v_10 (= x_44 2))) (let ((?v_237 (ite ?v_8 x_33 (ite ?v_9 x_32 (ite ?v_10 x_31 x_29)))) (?v_106 (not x_45)) (?v_142 (not x_47)) (?v_162 (not x_48)) (?v_182 (not x_49)) (?v_48 (< x_39 1)) (?v_236 (or (or (or x_45 x_47) x_48) x_49)) (?v_11 (= x_39 4))) (let ((?v_246 (ite ?v_11 1 (+ x_39 1))) (?v_12 (= x_40 4))) (let ((?v_247 (ite ?v_12 1 (+ x_40 1))) (?v_13 (= x_41 4))) (let ((?v_248 (ite ?v_13 1 (+ x_41 1))) (?v_14 (= x_42 4))) (let ((?v_249 (ite ?v_14 1 (+ x_42 1))) (?v_99 (= x_8 1)) (?v_4 (= x_18 4))) (let ((?v_57 (ite ?v_4 1 (+ x_18 1))) (?v_5 (= x_19 4))) (let ((?v_58 (ite ?v_5 1 (+ x_19 1))) (?v_6 (= x_20 4))) (let ((?v_59 (ite ?v_6 1 (+ x_20 1))) (?v_7 (= x_21 4))) (let ((?v_60 (ite ?v_7 1 (+ x_21 1))) (?v_81 (= x_47 x_10)) (?v_82 (= x_48 x_11)) (?v_83 (= x_49 x_12)) (?v_84 (= x_44 x_13)) (?v_137 (= x_40 x_13)) (?v_159 (= x_41 x_13)) (?v_72 (= x_28 x_4)) (?v_73 (= x_28 x_5)) (?v_74 (= x_28 x_6)) (?v_75 (= x_28 x_7)) (?v_179 (= x_42 x_13)) (?v_119 (= x_37 x_3)) (?v_120 (= x_42 x_21)) (?v_121 (= x_33 x_7)) (?v_86 (= x_34 x_0)) (?v_79 (= x_39 x_18)) (?v_87 (= x_29 x_4)) (?v_113 (= x_35 x_1)) (?v_114 (= x_40 x_19)) (?v_115 (= x_31 x_5)) (?v_116 (= x_36 x_2)) (?v_117 (= x_41 x_20)) (?v_118 (= x_32 x_6)) (?v_101 (= x_39 x_13)) (?v_70 (and (and (and ?v_61 ?v_62) ?v_63) ?v_64)) (?v_90 (= x_45 false)) (?v_128 (= x_47 false)) (?v_151 (= x_48 false)) (?v_171 (= x_49 false)) (?v_0 (= x_13 1)) (?v_217 (not x_14)) (?v_200 (not x_15))) (let ((?v_234 (and ?v_217 ?v_200)) (?v_201 (not x_16))) (let ((?v_186 (and ?v_234 ?v_201)) (?v_254 (and x_14 ?v_200)) (?v_256 (or x_14 x_15)) (?v_257 (or ?v_217 x_15))) (let ((?v_258 (and (and (and (and (and (or ?v_256 x_16) (or ?v_257 x_16)) (or (or x_14 ?v_200) x_16)) (or (or ?v_217 ?v_200) x_16)) (or ?v_256 ?v_201)) (or ?v_257 ?v_201))) (?v_65 (> x_4 0)) (?v_66 (> x_5 0)) (?v_67 (> x_6 0)) (?v_68 (> x_7 0)) (?v_187 (and (and (and ?v_106 ?v_142) ?v_162) ?v_182)) (?v_238 (or ?v_20 ?v_22)) (?v_240 (or ?v_21 ?v_32)) (?v_242 (or ?v_26 ?v_36)) (?v_244 (or ?v_29 ?v_39)) (?v_50 (and ?v_196 ?v_192)) (?v_51 (and ?v_197 ?v_193)) (?v_53 (and ?v_198 ?v_194)) (?v_54 (and ?v_199 ?v_195)) (?v_17 (+ x_28 3)) (?v_34 (+ x_29 3)) (?v_35 (+ x_31 3)) (?v_38 (+ x_32 3)) (?v_41 (+ x_33 3)) (?v_49 (+ (+ x_29 (* (ite ?v_48 (- (- 1 x_39) 1) (- (+ (- 4 x_39) 1) 1)) 3)) x_17)) (?v_52 (+ (+ x_31 (* (ite (< x_40 2) (- (- 2 x_40) 1) (- (+ (- 4 x_40) 2) 1)) 3)) x_17)) (?v_55 (+ (+ x_32 (* (ite (< x_41 3) (- (- 3 x_41) 1) (- (+ (- 4 x_41) 3) 1)) 3)) x_17)) (?v_56 (+ (+ x_33 (* (ite (< x_42 4) (- x_43 1) (- (+ x_43 4) 1)) 3)) x_17))) (let ((?v_235 (and (and (and (and (and (and (and (and (and (and (and (and (and ?v_187 (or (or (or ?v_15 ?v_16) ?v_18) ?v_19)) (or ?v_20 (<= x_29 ?v_17))) (or ?v_21 (<= x_31 ?v_17))) (or ?v_26 (<= x_32 ?v_17))) (or ?v_29 (<= x_33 ?v_17))) (or ?v_20 (and (and (and (or (or ?v_238 ?v_23) (and (= x_39 x_51) (= x_29 ?v_34))) (or ?v_21 (and (and (or (or ?v_22 ?v_32) (and ?v_24 (= x_29 x_31))) (or (or ?v_23 ?v_25) ?v_24)) (or (or ?v_22 ?v_25) (and (= x_39 x_52) (= x_29 ?v_35)))))) (or ?v_26 (and (and (or (or ?v_22 ?v_36) (and ?v_27 (= x_29 x_32))) (or (or ?v_23 ?v_28) ?v_27)) (or (or ?v_22 ?v_28) (and (= x_39 x_53) (= x_29 ?v_38)))))) (or ?v_29 (and (and (or (or ?v_22 ?v_39) (and ?v_30 (= x_29 x_33))) (or (or ?v_23 ?v_31) ?v_30)) (or (or ?v_22 ?v_31) (and (= x_39 x_54) (= x_29 ?v_41)))))))) (or ?v_21 (and (and (and (or ?v_20 (and (and (or (or ?v_32 ?v_22) (and ?v_33 (= x_31 x_29))) (or (or ?v_25 ?v_23) ?v_33)) (or (or ?v_32 ?v_23) (and (= x_40 x_51) (= x_31 ?v_34))))) (or (or ?v_240 ?v_25) (and (= x_40 x_52) (= x_31 ?v_35)))) (or ?v_26 (and (and (or (or ?v_32 ?v_36) (and ?v_37 (= x_31 x_32))) (or (or ?v_25 ?v_28) ?v_37)) (or (or ?v_32 ?v_28) (and (= x_40 x_53) (= x_31 ?v_38)))))) (or ?v_29 (and (and (or (or ?v_32 ?v_39) (and ?v_40 (= x_31 x_33))) (or (or ?v_25 ?v_31) ?v_40)) (or (or ?v_32 ?v_31) (and (= x_40 x_54) (= x_31 ?v_41)))))))) (or ?v_26 (and (and (and (or ?v_20 (and (and (or (or ?v_36 ?v_22) (and ?v_42 (= x_32 x_29))) (or (or ?v_28 ?v_23) ?v_42)) (or (or ?v_36 ?v_23) (and (= x_41 x_51) (= x_32 ?v_34))))) (or ?v_21 (and (and (or (or ?v_36 ?v_32) (and ?v_43 (= x_32 x_31))) (or (or ?v_28 ?v_25) ?v_43)) (or (or ?v_36 ?v_25) (and (= x_41 x_52) (= x_32 ?v_35)))))) (or (or ?v_242 ?v_28) (and (= x_41 x_53) (= x_32 ?v_38)))) (or ?v_29 (and (and (or (or ?v_36 ?v_39) (and ?v_44 (= x_32 x_33))) (or (or ?v_28 ?v_31) ?v_44)) (or (or ?v_36 ?v_31) (and (= x_41 x_54) (= x_32 ?v_41)))))))) (or ?v_29 (and (and (and (or ?v_20 (and (and (or (or ?v_39 ?v_22) (and ?v_45 (= x_33 x_29))) (or (or ?v_31 ?v_23) ?v_45)) (or (or ?v_39 ?v_23) (and (= x_42 x_51) (= x_33 ?v_34))))) (or ?v_21 (and (and (or (or ?v_39 ?v_32) (and ?v_46 (= x_33 x_31))) (or (or ?v_31 ?v_25) ?v_46)) (or (or ?v_39 ?v_25) (and (= x_42 x_52) (= x_33 ?v_35)))))) (or ?v_26 (and (and (or (or ?v_39 ?v_36) (and ?v_47 (= x_33 x_32))) (or (or ?v_31 ?v_28) ?v_47)) (or (or ?v_39 ?v_28) (and (= x_42 x_53) (= x_33 ?v_38)))))) (or (or ?v_244 ?v_31) (and (= x_42 x_54) (= x_33 ?v_41)))))) (or ?v_20 (and (and (and (or ?v_50 (not (<= x_29 ?v_49))) (or ?v_51 (not (<= x_31 ?v_49)))) (or ?v_53 (not (<= x_32 ?v_49)))) (or ?v_54 (not (<= x_33 ?v_49)))))) (or ?v_21 (and (and (and (or ?v_50 (not (<= x_29 ?v_52))) (or ?v_51 (not (<= x_31 ?v_52)))) (or ?v_53 (not (<= x_32 ?v_52)))) (or ?v_54 (not (<= x_33 ?v_52)))))) (or ?v_26 (and (and (and (or ?v_50 (not (<= x_29 ?v_55))) (or ?v_51 (not (<= x_31 ?v_55)))) (or ?v_53 (not (<= x_32 ?v_55)))) (or ?v_54 (not (<= x_33 ?v_55)))))) (or ?v_29 (and (and (and (or ?v_50 (not (<= x_29 ?v_56))) (or ?v_51 (not (<= x_31 ?v_56)))) (or ?v_53 (not (<= x_32 ?v_56)))) (or ?v_54 (not (<= x_33 ?v_56))))))) (?v_69 (and (and (and ?v_65 ?v_66) ?v_67) ?v_68)) (?v_71 (and (and (and (<= x_28 x_4) (<= x_28 x_5)) (<= x_28 x_6)) (<= x_28 x_7))) (?v_185 (= x_28 0)) (?v_80 (and (= x_38 x_8) (= x_46 0)))) (let ((?v_124 (and ?v_80 (= x_45 x_9)))) (let ((?v_147 (and ?v_124 ?v_81))) (let ((?v_167 (and ?v_147 ?v_82)) (?v_85 (= x_30 0))) (let ((?v_78 (and (and (and ?v_167 ?v_83) ?v_84) ?v_85)) (?v_88 (= 0 x_4)) (?v_92 (= 0 0)) (?v_94 (and (and (and (and (and (and ?v_80 ?v_90) ?v_81) ?v_82) ?v_83) ?v_84) ?v_85)) (?v_93 (+ 0 12))) (let ((?v_97 (= x_29 ?v_93)) (?v_105 (= x_46 (ite ?v_70 (+ 0 x_17) 0)))) (let ((?v_127 (and (= x_38 (ite ?v_70 0 x_8)) ?v_105)) (?v_107 (= x_47 (or ?v_70 x_10))) (?v_108 (= x_48 (or ?v_70 x_11))) (?v_109 (= x_49 (or ?v_70 x_12))) (?v_110 (= x_44 (ite ?v_70 1 x_13))) (?v_111 (= x_30 (ite ?v_70 0 0)))) (let ((?v_98 (and (and (and (and (and (and ?v_127 ?v_90) ?v_107) ?v_108) ?v_109) ?v_110) ?v_111)) (?v_102 (+ 0 3))) (let ((?v_132 (- ?v_102 x_17))) (let ((?v_100 (= x_29 ?v_132)) (?v_103 (and ?v_112 ?v_88)) (?v_104 (= x_29 ?v_102)) (?v_140 (= x_38 (ite ?v_70 1 x_8))) (?v_125 (= 0 x_5)) (?v_131 (and (and (and (and (and ?v_124 ?v_128) ?v_82) ?v_83) ?v_84) ?v_85)) (?v_130 (+ 0 15))) (let ((?v_134 (= x_31 ?v_130)) (?v_141 (= x_45 (or ?v_70 x_9)))) (let ((?v_150 (and ?v_127 ?v_141)) (?v_143 (= x_44 (ite ?v_70 2 x_13)))) (let ((?v_135 (and (and (and (and (and ?v_150 ?v_128) ?v_108) ?v_109) ?v_143) ?v_111)) (?v_136 (= x_31 ?v_132)) (?v_138 (and ?v_144 ?v_125)) (?v_139 (= x_31 ?v_102)) (?v_148 (= 0 x_6)) (?v_154 (and (and (and (and ?v_147 ?v_151) ?v_83) ?v_84) ?v_85)) (?v_153 (+ 0 18))) (let ((?v_156 (= x_32 ?v_153)) (?v_170 (and ?v_150 ?v_107)) (?v_163 (= x_44 (ite ?v_70 3 x_13)))) (let ((?v_157 (and (and (and (and ?v_170 ?v_151) ?v_109) ?v_163) ?v_111)) (?v_158 (= x_32 ?v_132)) (?v_160 (and ?v_164 ?v_148)) (?v_161 (= x_32 ?v_102)) (?v_168 (= 0 x_7)) (?v_174 (and (and (and ?v_167 ?v_171) ?v_84) ?v_85)) (?v_173 (+ 0 21))) (let ((?v_176 (= x_33 ?v_173)) (?v_183 (= x_44 (ite ?v_70 4 x_13)))) (let ((?v_177 (and (and (and (and ?v_170 ?v_108) ?v_171) ?v_183) ?v_111)) (?v_178 (= x_33 ?v_132)) (?v_180 (and ?v_184 ?v_168)) (?v_181 (= x_33 ?v_102)) (?v_188 (or (= x_34 0) ?v_77)) (?v_189 (or (= x_35 0) ?v_123)) (?v_190 (or (= x_36 0) ?v_146)) (?v_191 (or (= x_37 0) ?v_166)) (?v_219 (and (and ?v_236 (= x_38 0)) (= x_50 2)))) (let ((?v_203 (or ?v_188 ?v_89)) (?v_204 (or ?v_189 ?v_126)) (?v_205 (or ?v_190 ?v_149)) (?v_206 (or ?v_191 ?v_169))) (let ((?v_202 (and (and (and (and (and (and (and (and (and (and (and (and ?v_219 ?v_203) ?v_204) ?v_205) ?v_206) (or ?v_192 (and (and ?v_106 ?v_220) ?v_207))) (or ?v_193 (and (and ?v_142 ?v_221) ?v_208))) (or ?v_194 (and (and ?v_162 ?v_222) ?v_209))) (or ?v_195 (and (and ?v_182 ?v_223) ?v_210))) (or (or ?v_196 x_45) ?v_225)) (or (or ?v_197 x_47) ?v_227)) (or (or ?v_198 x_48) ?v_229)) (or (or ?v_199 x_49) ?v_231))) (?v_218 (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and ?v_187 (or (or (or ?v_89 ?v_126) ?v_149) ?v_169)) ?v_203) ?v_204) ?v_205) ?v_206) (or ?v_192 ?v_207)) (or ?v_193 ?v_208)) (or ?v_194 ?v_209)) (or ?v_195 ?v_210)) (or ?v_192 (and (and (or ?v_193 ?v_211) (or ?v_194 ?v_212)) (or ?v_195 ?v_213)))) (or ?v_193 (and (or ?v_194 ?v_214) (or ?v_195 ?v_215)))) (or (or ?v_194 ?v_195) ?v_216)) (or ?v_192 (and (and (and (or ?v_196 (not (<= (- x_29 x_29) x_17))) (or ?v_197 ?v_211)) (or ?v_198 ?v_212)) (or ?v_199 ?v_213)))) (or ?v_193 (and (and (and (or ?v_196 (not (<= (- x_29 x_31) x_17))) (or ?v_197 (not (<= (- x_31 x_31) x_17)))) (or ?v_198 ?v_214)) (or ?v_199 ?v_215)))) (or ?v_194 (and (and (and (or ?v_196 (not (<= (- x_29 x_32) x_17))) (or ?v_197 (not (<= (- x_31 x_32) x_17)))) (or ?v_198 (not (<= (- x_32 x_32) x_17)))) (or ?v_199 ?v_216)))) (or ?v_195 (and (and (and (or ?v_196 (not (<= (- x_29 x_33) x_17))) (or ?v_197 (not (<= (- x_31 x_33) x_17)))) (or ?v_198 (not (<= (- x_32 x_33) x_17)))) (or ?v_199 (not (<= (- x_33 x_33) x_17))))))) (?v_250 (or (or ?v_196 ?v_224) ?v_225)) (?v_251 (or (or ?v_197 ?v_226) ?v_227)) (?v_252 (or (or ?v_198 ?v_228) ?v_229)) (?v_253 (or (or ?v_199 ?v_230) ?v_231)) (?v_232 (+ x_30 3))) (let ((?v_233 (and (and (and (and (and (and (and (and (and (and (and (and (and (and ?v_219 (= ?v_237 (+ (+ x_30 (* (- x_44 1) 3)) 12))) (not (ite ?v_8 x_49 (ite ?v_9 x_48 (ite ?v_10 x_47 x_45))))) (or (or (or ?v_192 (= 1 x_44)) ?v_224) (and ?v_220 ?v_207))) (or (or (or ?v_193 (= 2 x_44)) ?v_226) (and ?v_221 ?v_208))) (or (or (or ?v_194 (= 3 x_44)) ?v_228) (and ?v_222 ?v_209))) (or (or (or ?v_195 (= 4 x_44)) ?v_230) (and ?v_223 ?v_210))) ?v_250) ?v_251) ?v_252) ?v_253) (or ?v_20 (and ?v_239 (= x_29 ?v_232)))) (or ?v_21 (and ?v_241 (= x_31 ?v_232)))) (or ?v_26 (and ?v_243 (= x_32 ?v_232)))) (or ?v_29 (and ?v_245 (= x_33 ?v_232))))) (?v_255 (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and ?v_236 (= x_38 1)) (= x_50 3)) (= (ite ?v_8 x_42 (ite ?v_9 x_41 (ite ?v_10 x_40 x_39))) x_44)) (= ?v_237 ?v_232)) (or ?v_238 (and ?v_239 (= x_29 ?v_237)))) (or ?v_240 (and ?v_241 (= x_31 ?v_237)))) (or ?v_242 (and ?v_243 (= x_32 ?v_237)))) (or ?v_244 (and ?v_245 (= x_33 ?v_237)))) (or (or ?v_20 ?v_23) (and (= ?v_246 x_44) (= ?v_237 ?v_34)))) (or (or ?v_21 ?v_25) (and (= ?v_247 x_44) (= ?v_237 ?v_35)))) (or (or ?v_26 ?v_28) (and (= ?v_248 x_44) (= ?v_237 ?v_38)))) (or (or ?v_29 ?v_31) (and (= ?v_249 x_44) (= ?v_237 ?v_41)))) ?v_250) ?v_251) ?v_252) ?v_253) (or ?v_192 ?v_224)) (or ?v_193 ?v_226)) (or ?v_194 ?v_228)) (or ?v_195 ?v_230)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (<= x_60 6) (>= x_60 0)) (<= x_55 6)) (>= x_55 0)) (<= x_50 3)) (>= x_50 0)) (<= x_38 1)) (>= x_38 0)) (<= x_37 3)) (>= x_37 0)) (<= x_36 3)) (>= x_36 0)) (<= x_35 3)) (>= x_35 0)) (<= x_34 3)) (>= x_34 0)) (<= x_23 3)) (>= x_23 0)) (<= x_8 1)) (>= x_8 0)) (<= x_3 3)) (>= x_3 0)) (<= x_2 3)) (>= x_2 0)) (<= x_1 3)) (>= x_1 0)) (<= x_0 3)) (>= x_0 0)) (or (or (or ?v_0 ?v_3) ?v_2) ?v_1)) (not (< x_13 1))) (<= x_13 4)) (> x_17 0)) (< x_17 (/ 3 2))) (or (or (or (= x_18 1) (= x_18 2)) (= x_18 3)) ?v_4)) (not (< x_18 1))) (<= x_18 4)) (or (or (or (= x_19 1) (= x_19 2)) (= x_19 3)) ?v_5)) (not (< x_19 1))) (<= x_19 4)) (or (or (or (= x_20 1) (= x_20 2)) (= x_20 3)) ?v_6)) (not (< x_20 1))) (<= x_20 4)) (or (or (or (= x_21 1) (= x_21 2)) (= x_21 3)) ?v_7)) (not (< x_21 1))) (<= x_21 4)) (or (or (or (= x_39 1) (= x_39 2)) (= x_39 3)) ?v_11)) (not ?v_48)) (<= x_39 4)) (or (or (or (= x_40 1) (= x_40 2)) (= x_40 3)) ?v_12)) (not (< x_40 1))) (<= x_40 4)) (or (or (or (= x_41 1) (= x_41 2)) (= x_41 3)) ?v_13)) (not (< x_41 1))) (<= x_41 4)) (or (or (or (= x_42 1) (= x_42 2)) (= x_42 3)) ?v_14)) (not (< x_42 1))) (<= x_42 4)) (or (or (or (= x_44 1) ?v_10) ?v_9) ?v_8)) (not (< x_44 1))) (<= x_44 4)) ?v_76) ?v_122) ?v_145) ?v_165) ?v_65) (< x_4 30)) ?v_66) (< x_5 30)) ?v_67) (< x_6 30)) ?v_68) (< x_7 30)) ?v_99) ?v_61) ?v_62) ?v_63) ?v_64) ?v_0) ?v_186) (= x_22 (- 4 x_21))) (= x_23 (ite ?v_1 x_3 (ite ?v_2 x_2 (ite ?v_3 x_1 x_0))))) (= x_24 ?v_57)) (= x_25 ?v_58)) (= x_26 ?v_59)) (= x_27 ?v_60)) (= x_43 (- 4 x_42))) (= x_50 (ite ?v_8 x_37 (ite ?v_9 x_36 (ite ?v_10 x_35 x_34))))) (= x_51 ?v_246)) (= x_52 ?v_247)) (= x_53 ?v_248)) (= x_54 ?v_249)) (= x_55 (ite ?v_235 4 6))) (= x_56 ?v_57)) (= x_57 ?v_58)) (= x_58 ?v_59)) (= x_59 ?v_60)) (or (and (and (and (and (and (and (and (and (and (and (and (and (and (and (ite ?v_70 ?v_69 (and ?v_69 (> 0 0))) (ite ?v_70 (and ?v_71 (or (or (or ?v_72 ?v_73) ?v_74) ?v_75)) (and (and ?v_71 (<= x_28 0)) (or (or (or (or ?v_185 ?v_72) ?v_73) ?v_74) ?v_75)))) ?v_86) ?v_113) ?v_116) ?v_119) ?v_79) ?v_114) ?v_117) ?v_120) ?v_87) ?v_115) ?v_118) ?v_121) ?v_78) (and (or (or (or (and (and (and (and (and (and (and (and (and (or (or (or (or (or (or (or (or (or (and (and (and (and (and ?v_76 ?v_88) ?v_77) (= x_29 (+ 0 24))) ?v_78) ?v_79) (and (and (and (and (and (and ?v_76 x_9) ?v_92) ?v_94) ?v_86) ?v_79) ?v_87)) (and (and (and (and (and ?v_91 ?v_88) ?v_89) ?v_97) ?v_98) ?v_79)) (and (and (and (and (and (and (and ?v_91 x_9) ?v_95) ?v_92) ?v_89) (= x_29 (- ?v_93 x_17))) ?v_94) ?v_79)) (and (and (and (and (and (and (and ?v_96 x_9) ?v_95) ?v_92) ?v_15) ?v_100) ?v_101) ?v_94)) (and (and (and (and (and ?v_96 ?v_88) ?v_97) ?v_98) ?v_86) ?v_79)) (and (and (and (and (and (and (and (or ?v_91 ?v_96) x_9) ?v_99) ?v_92) ?v_15) ?v_100) ?v_101) ?v_94)) (and (and (and (and (and ?v_103 (not (= ?v_57 1))) ?v_104) (= x_39 x_56)) ?v_78) ?v_86)) (and (and (and (and (and (and (and (and (and (and (and (and ?v_103 (= x_56 1)) ?v_104) (= x_39 ?v_57)) ?v_140) ?v_105) ?v_106) ?v_107) ?v_108) ?v_109) ?v_110) ?v_111) ?v_86)) (and (and (and (and (and (and (and ?v_112 x_9) ?v_99) ?v_92) ?v_94) ?v_86) ?v_79) ?v_87)) ?v_113) ?v_114) ?v_115) ?v_116) ?v_117) ?v_118) ?v_119) ?v_120) ?v_121) (and (and (and (and (and (and (and (and (and (or (or (or (or (or (or (or (or (or (and (and (and (and (and ?v_122 ?v_125) ?v_123) (= x_31 (+ 0 27))) ?v_78) ?v_114) (and (and (and (and (and (and ?v_122 x_10) ?v_92) ?v_131) ?v_113) ?v_114) ?v_115)) (and (and (and (and (and ?v_129 ?v_125) ?v_126) ?v_134) ?v_135) ?v_114)) (and (and (and (and (and (and (and ?v_129 x_10) ?v_95) ?v_92) ?v_126) (= x_31 (- ?v_130 x_17))) ?v_131) ?v_114)) (and (and (and (and (and (and (and ?v_133 x_10) ?v_95) ?v_92) ?v_16) ?v_136) ?v_137) ?v_131)) (and (and (and (and (and ?v_133 ?v_125) ?v_134) ?v_135) ?v_113) ?v_114)) (and (and (and (and (and (and (and (or ?v_129 ?v_133) x_10) ?v_99) ?v_92) ?v_16) ?v_136) ?v_137) ?v_131)) (and (and (and (and (and ?v_138 (not (= ?v_58 2))) ?v_139) (= x_40 x_57)) ?v_78) ?v_113)) (and (and (and (and (and (and (and (and (and (and (and (and ?v_138 (= x_57 2)) ?v_139) (= x_40 ?v_58)) ?v_140) ?v_105) ?v_141) ?v_142) ?v_108) ?v_109) ?v_143) ?v_111) ?v_113)) (and (and (and (and (and (and (and ?v_144 x_10) ?v_99) ?v_92) ?v_131) ?v_113) ?v_114) ?v_115)) ?v_86) ?v_79) ?v_87) ?v_116) ?v_117) ?v_118) ?v_119) ?v_120) ?v_121)) (and (and (and (and (and (and (and (and (and (or (or (or (or (or (or (or (or (or (and (and (and (and (and ?v_145 ?v_148) ?v_146) (= x_32 (+ 0 30))) ?v_78) ?v_117) (and (and (and (and (and (and ?v_145 x_11) ?v_92) ?v_154) ?v_116) ?v_117) ?v_118)) (and (and (and (and (and ?v_152 ?v_148) ?v_149) ?v_156) ?v_157) ?v_117)) (and (and (and (and (and (and (and ?v_152 x_11) ?v_95) ?v_92) ?v_149) (= x_32 (- ?v_153 x_17))) ?v_154) ?v_117)) (and (and (and (and (and (and (and ?v_155 x_11) ?v_95) ?v_92) ?v_18) ?v_158) ?v_159) ?v_154)) (and (and (and (and (and ?v_155 ?v_148) ?v_156) ?v_157) ?v_116) ?v_117)) (and (and (and (and (and (and (and (or ?v_152 ?v_155) x_11) ?v_99) ?v_92) ?v_18) ?v_158) ?v_159) ?v_154)) (and (and (and (and (and ?v_160 (not (= ?v_59 3))) ?v_161) (= x_41 x_58)) ?v_78) ?v_116)) (and (and (and (and (and (and (and (and (and (and (and (and ?v_160 (= x_58 3)) ?v_161) (= x_41 ?v_59)) ?v_140) ?v_105) ?v_141) ?v_107) ?v_162) ?v_109) ?v_163) ?v_111) ?v_116)) (and (and (and (and (and (and (and ?v_164 x_11) ?v_99) ?v_92) ?v_154) ?v_116) ?v_117) ?v_118)) ?v_86) ?v_79) ?v_87) ?v_113) ?v_114) ?v_115) ?v_119) ?v_120) ?v_121)) (and (and (and (and (and (and (and (and (and (or (or (or (or (or (or (or (or (or (and (and (and (and (and ?v_165 ?v_168) ?v_166) (= x_33 (+ 0 33))) ?v_78) ?v_120) (and (and (and (and (and (and ?v_165 x_12) ?v_92) ?v_174) ?v_119) ?v_120) ?v_121)) (and (and (and (and (and ?v_172 ?v_168) ?v_169) ?v_176) ?v_177) ?v_120)) (and (and (and (and (and (and (and ?v_172 x_12) ?v_95) ?v_92) ?v_169) (= x_33 (- ?v_173 x_17))) ?v_174) ?v_120)) (and (and (and (and (and (and (and ?v_175 x_12) ?v_95) ?v_92) ?v_19) ?v_178) ?v_179) ?v_174)) (and (and (and (and (and ?v_175 ?v_168) ?v_176) ?v_177) ?v_119) ?v_120)) (and (and (and (and (and (and (and (or ?v_172 ?v_175) x_12) ?v_99) ?v_92) ?v_19) ?v_178) ?v_179) ?v_174)) (and (and (and (and (and ?v_180 (not (= ?v_60 4))) ?v_181) (= x_42 x_59)) ?v_78) ?v_119)) (and (and (and (and (and (and (and (and (and (and (and (and ?v_180 (= x_59 4)) ?v_181) (= x_42 ?v_60)) ?v_140) ?v_105) ?v_141) ?v_107) ?v_108) ?v_182) ?v_183) ?v_111) ?v_119)) (and (and (and (and (and (and (and ?v_184 x_12) ?v_99) ?v_92) ?v_174) ?v_119) ?v_120) ?v_121)) ?v_86) ?v_79) ?v_87) ?v_113) ?v_114) ?v_115) ?v_116) ?v_117) ?v_118)) ?v_185))) (or (or (or (or (or (or (and ?v_186 (= x_60 (ite (and (and (and (and ?v_187 ?v_188) ?v_189) ?v_190) ?v_191) 0 (ite ?v_202 1 6)))) (and (and ?v_254 ?v_201) (= x_60 (ite ?v_202 1 (ite ?v_218 2 6))))) (and (and (and ?v_217 x_15) ?v_201) (= x_60 (ite ?v_218 2 (ite ?v_233 3 6))))) (and (and (and x_14 x_15) ?v_201) (= x_60 (ite ?v_233 3 (ite ?v_218 2 x_55))))) (and (and ?v_234 x_16) (= x_60 (ite ?v_235 4 (ite ?v_255 5 6))))) (and (and ?v_254 x_16) (= x_60 (ite ?v_255 5 x_55)))) (and ?v_258 (= x_60 6)))) (or (and (and (and (and (and (not (= x_60 0)) (not (= x_60 1))) (not (= x_60 2))) (not (= x_60 3))) (not (= x_60 4))) (not (= x_60 5))) ?v_258)) (or (or ?v_201 ?v_200) ?v_217)))))))))))))))))))))))))))))))))))))))))
(check-sat)
(exit)
